(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 12))
(let ((e4 7))
(let ((e5 1))
(let ((e6 (- v2)))
(let ((e7 (- v1 v2)))
(let ((e8 (- e7)))
(let ((e9 (- e6)))
(let ((e10 (/ e3 (- e4))))
(let ((e11 (- e7)))
(let ((e12 (- v1 e8)))
(let ((e13 (* (- e5) v1)))
(let ((e14 (+ e7 e12)))
(let ((e15 (* e13 e13)))
(let ((e16 (- e7)))
(let ((e17 (+ e14 e7)))
(let ((e18 (+ e11 v1)))
(let ((e19 (/ e4 e5)))
(let ((e20 (- v1 v2)))
(let ((e21 (/ e3 e3)))
(let ((e22 (- e9 v0)))
(let ((e23 (< e21 e20)))
(let ((e24 (> e14 e7)))
(let ((e25 (< e18 e14)))
(let ((e26 (< e22 e11)))
(let ((e27 (= e15 e10)))
(let ((e28 (>= e13 e14)))
(let ((e29 (<= e12 e20)))
(let ((e30 (distinct e10 v2)))
(let ((e31 (>= e6 e11)))
(let ((e32 (distinct e12 e8)))
(let ((e33 (<= e16 e22)))
(let ((e34 (distinct v0 e12)))
(let ((e35 (> v2 v1)))
(let ((e36 (= e11 e6)))
(let ((e37 (>= e16 e11)))
(let ((e38 (<= v2 e7)))
(let ((e39 (> e21 e6)))
(let ((e40 (>= e10 e7)))
(let ((e41 (< e17 e20)))
(let ((e42 (<= e19 e21)))
(let ((e43 (< e10 e19)))
(let ((e44 (< e11 e16)))
(let ((e45 (>= e6 e20)))
(let ((e46 (> e18 e18)))
(let ((e47 (>= e15 e8)))
(let ((e48 (<= e14 e17)))
(let ((e49 (> e18 e15)))
(let ((e50 (distinct e18 e20)))
(let ((e51 (distinct v1 e13)))
(let ((e52 (> e12 e6)))
(let ((e53 (<= e9 e18)))
(let ((e54 (= e12 v2)))
(let ((e55 (distinct e6 e12)))
(let ((e56 (<= e9 e16)))
(let ((e57 (>= e9 e10)))
(let ((e58 (distinct e12 e16)))
(let ((e59 (< e13 e21)))
(let ((e60 (= e20 e14)))
(let ((e61 (< e6 e6)))
(let ((e62 (distinct e17 e20)))
(let ((e63 (= e18 e14)))
(let ((e64 (< e22 e13)))
(let ((e65 (> e15 e19)))
(let ((e66 (> e14 e17)))
(let ((e67 (<= e6 e12)))
(let ((e68 (>= e7 e12)))
(let ((e69 (<= e9 e19)))
(let ((e70 (distinct e21 v2)))
(let ((e71 (<= e9 e16)))
(let ((e72 (distinct e13 e21)))
(let ((e73 (= e15 e17)))
(let ((e74 (> e13 e14)))
(let ((e75 (> e20 e12)))
(let ((e76 (>= e7 v1)))
(let ((e77 (distinct v0 v2)))
(let ((e78 (> v0 e9)))
(let ((e79 (= e18 e9)))
(let ((e80 (<= e13 e22)))
(let ((e81 (= e8 v1)))
(let ((e82 (> e15 e8)))
(let ((e83 (distinct e9 e17)))
(let ((e84 (= e22 e9)))
(let ((e85 (distinct e20 e12)))
(let ((e86 (= v0 e6)))
(let ((e87 (= e7 v2)))
(let ((e88 (< e19 e20)))
(let ((e89 (= e17 v0)))
(let ((e90 (<= e6 e8)))
(let ((e91 (< e22 v0)))
(let ((e92 (= e16 e6)))
(let ((e93 (<= e21 e17)))
(let ((e94 (< e11 e16)))
(let ((e95 (and e25 e87)))
(let ((e96 (ite e70 e39 e47)))
(let ((e97 (ite e26 e65 e65)))
(let ((e98 (not e76)))
(let ((e99 (=> e54 e50)))
(let ((e100 (= e71 e66)))
(let ((e101 (xor e27 e83)))
(let ((e102 (and e90 e95)))
(let ((e103 (= e53 e69)))
(let ((e104 (ite e72 e57 e28)))
(let ((e105 (or e100 e58)))
(let ((e106 (and e84 e46)))
(let ((e107 (= e64 e60)))
(let ((e108 (= e49 e106)))
(let ((e109 (xor e51 e38)))
(let ((e110 (and e103 e109)))
(let ((e111 (or e93 e93)))
(let ((e112 (not e56)))
(let ((e113 (=> e36 e88)))
(let ((e114 (xor e30 e112)))
(let ((e115 (=> e32 e80)))
(let ((e116 (xor e24 e34)))
(let ((e117 (not e97)))
(let ((e118 (= e102 e102)))
(let ((e119 (and e45 e115)))
(let ((e120 (= e78 e78)))
(let ((e121 (= e85 e31)))
(let ((e122 (xor e29 e74)))
(let ((e123 (= e63 e75)))
(let ((e124 (or e23 e77)))
(let ((e125 (= e99 e123)))
(let ((e126 (=> e94 e111)))
(let ((e127 (= e86 e116)))
(let ((e128 (xor e125 e79)))
(let ((e129 (or e114 e68)))
(let ((e130 (= e124 e33)))
(let ((e131 (and e91 e108)))
(let ((e132 (ite e41 e37 e42)))
(let ((e133 (xor e62 e129)))
(let ((e134 (xor e107 e55)))
(let ((e135 (= e96 e127)))
(let ((e136 (xor e67 e119)))
(let ((e137 (and e44 e118)))
(let ((e138 (=> e89 e136)))
(let ((e139 (=> e132 e105)))
(let ((e140 (or e35 e98)))
(let ((e141 (xor e121 e104)))
(let ((e142 (xor e110 e135)))
(let ((e143 (= e133 e52)))
(let ((e144 (ite e134 e43 e82)))
(let ((e145 (or e59 e144)))
(let ((e146 (ite e61 e130 e117)))
(let ((e147 (=> e40 e139)))
(let ((e148 (=> e141 e81)))
(let ((e149 (xor e126 e147)))
(let ((e150 (and e149 e113)))
(let ((e151 (=> e122 e138)))
(let ((e152 (not e48)))
(let ((e153 (not e142)))
(let ((e154 (xor e131 e131)))
(let ((e155 (=> e137 e128)))
(let ((e156 (= e148 e92)))
(let ((e157 (= e145 e154)))
(let ((e158 (and e143 e101)))
(let ((e159 (= e151 e150)))
(let ((e160 (xor e159 e158)))
(let ((e161 (= e160 e157)))
(let ((e162 (not e146)))
(let ((e163 (or e152 e162)))
(let ((e164 (and e140 e140)))
(let ((e165 (xor e164 e161)))
(let ((e166 (and e155 e120)))
(let ((e167 (xor e166 e153)))
(let ((e168 (or e73 e163)))
(let ((e169 (= e165 e167)))
(let ((e170 (not e169)))
(let ((e171 (=> e168 e170)))
(let ((e172 (xor e156 e171)))
e172
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
